『Metaprogramming in Lean』
ondanaoto/japanese-translation-lean4-metaprogramming-book
Introduction - Metaprogramming in Lean 4
マクロ関連は下記も見るとよい
『Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages』
Metaprogramming in Lean ログ
#Leanドキュメント
#文献